#ifndef __INEQUALITY_GRAPH__
#define __INEQUALITY_GRAPH__

#include <vector>
#include <map>
#include <stack>
#include "llvm/Support/raw_ostream.h"
#include "llvm/Instructions.h"
#include "LLVMCompat.h"

using std::map;

namespace llvm {

class Value;

PHINode* isPHINode(Value*);
bool isPINode(PHINode*);

struct IGEdge;

std::pair<bool, int> isConstInt(Value*);

enum VertexType {
	None, Phi, Add, Mul
};

struct IGVertex {
	IGVertex(Value* v, VertexType t = None) :
			value(v), type(t) {
	}

	Value* value;
	VertexType type;
	std::vector<IGEdge*> inEdges;
	std::vector<IGEdge*> outEdges;
};

struct AddVertex: IGVertex {
	Value* LHS;
	Value* RHS;
	AddVertex(Value* Res, Value* lhs, Value* rhs) :
			IGVertex(Res, Add), LHS(lhs), RHS(rhs) {
	}
};

struct MulVertex: IGVertex {
	Value* Coeff;
	Value* Var;
	/*
	 *Represent a node Res = C op Var. C is the coefficient and var is the variable
	 */
	MulVertex(Value* Res, Value* C, Value* Var) :
			IGVertex(Res, Mul), Coeff(C), Var(Var) {
	}
};

struct IGEdge {
	IGEdge() :
			source(NULL), target(NULL), weight(0) {
	}
	IGEdge(IGVertex* src, IGVertex* tgt, int w) :
			source(src), target(tgt), weight(w) {
		src->outEdges.push_back(this);
		tgt->inEdges.push_back(this);
	}

	IGVertex* source;
	IGVertex* target;
	int weight;
};

struct Triple {
	Triple(Value* x, Value* y, int z) :
			a(x), v(y), c(z) {
	}

	Value* a;
	Value* v;
	int c;
};

inline bool operator <(const Triple& t1, const Triple& t2) {
	if (t1.a == t2.a) {
		if (t1.v == t2.v)
			return t1.c < t2.c;
		else
			return t1.v < t2.v;
	} else
		return t1.a < t2.a;
}

bool isPhiNode(Value* v) {
	PHINode* phi = dyn_cast<PHINode>(v);
	if (phi != 0) {
		return phi->getNumIncomingValues() > 1;
	}
	return false;
}

bool isPiNode(Value* v) {
	PHINode* phi = dyn_cast<PHINode>(v);
	if (phi != 0) {
		return phi->getNumIncomingValues() == 1;
	}
	return false;
}

bool isPhiNotPiNode(Value* v) {
	PHINode* phi = dyn_cast<PHINode>(v);
	if (phi != NULL) {
		return phi->getNumIncomingValues() != 1;
	}
    return false;
}

enum Result {
	False = 0, Reduced, True
};

struct InequalityGraph {
	map<Value*, IGVertex*> vertices;
	std::set<IGEdge*> edges;

public:
	IGVertex* addVertex(Value* val) {
		map<Value*, IGVertex*>::iterator iter = vertices.find(val);
		if (iter == vertices.end()) {
			IGVertex* vertex = new IGVertex(val);
			if(isPhiNode(val))
				vertex->type = Phi;
			else
				vertex->type = None;
			vertices[val] = vertex;
			return vertex;
		} else
			return iter->second;
	}

	void addVertex(IGVertex* v) {
		vertices[v->value] = v;
	}

	void addEdge(IGVertex* src, IGVertex* tgt, int weight) {
		IGEdge* edge = new IGEdge(src, tgt, weight);
		edges.insert(edge);
	}

	void addEdge(Value* src, Value* tgt, int weight) {
		if (src == NULL || tgt == NULL)
			return;
		IGEdge* edge = new IGEdge(addVertex(src), addVertex(tgt), weight);
		edges.insert(edge);
		if (MY_DEBUG) {
			errs() << "Added an edge: ";
			src->print(errs());
			errs() << " ";
			tgt->print(errs());
			errs() << '\t' << weight << '\n';
		}
	}

	bool demandProve(Value* index, Value* length) {
		C.clear();
		active.clear();

		Result r = prove(length, index, -1);
		if (r == True || r == Reduced)
			return true;
		else
			return false;
	}

	int getMaxValue(Value* val) {
        std::set<IGVertex*> searched;
        //std::map<IGVertex*, bool> active;
        return getMaxValue(val, searched);
    }

	int getMaxValue(Value* val, std::set<IGVertex*> searched) {
		int maxVal = 10000000;
		if (vertices.count(val) == 0)
			// Returns a farely large value. We cannot use the max value of int since
			// we don't want overflow for any operation on it.
			return maxVal;

		IGVertex* vertex = vertices[val];

        if (searched.count(vertex) > 0)
            return maxVal;

        searched.insert(vertex);

        std::pair<bool, int> res = isConstInt(vertex->value);
        if (res.first)
            return res.second;

        if (vertex->type == Add)
        {
            AddVertex* addVertex = static_cast<AddVertex*>(vertex);
            return getMaxValue(addVertex->LHS, searched) + getMaxValue(addVertex->RHS, searched);
        }

        else if (vertex->type == Mul)
        {
            MulVertex* mulVertex = static_cast<MulVertex*>(vertex);
            std::pair<bool, int> res = isConstInt(mulVertex->Coeff);
            if (res.first)
            {
                int co = isConstInt(mulVertex->Coeff).second;
                int result = co * getMaxValue(mulVertex->Var, searched);
                errs() << "\nMIN: " << result << '\n';
                vertex->value->print(errs());
                return result;
            }
        }

#if 1
        if (isPhiNotPiNode(vertex->value))
        //else if (vertex->type == Phi)
        {
            int minVal = -10000000;
            std::vector<IGEdge*> inEdges = vertex->inEdges;
            if (inEdges.empty())
                return maxVal;
            for (size_t i = 0; i < inEdges.size(); ++i)
            {
                int  maxv = getMaxValue(inEdges[i]->source->value, searched);
                minVal = std::max(minVal, maxv + inEdges[i]->weight);
                errs() << "\nMIN: " << minVal << '\n';
                vertex->value->print(errs());
            }
            return minVal;
        }
#endif


		// Search in the graph for its minimum value.
		//std::set<IGVertex*> searched;
        //std::stack<IGVertex*> toBeSearched;

        std::vector<IGEdge*> inEdges = vertex->inEdges;
        for (size_t i = 0; i < inEdges.size(); ++i) 
        {
            maxVal = std::min(maxVal, getMaxValue(inEdges[i]->source->value, searched) + inEdges[i]->weight);
                errs() << "\nMAX: " << maxVal << '\n';
                vertex->value->print(errs());
        }

        return maxVal;

#if 0

		toBeSearched.push(vertex);

		while (!toBeSearched.empty()) {
			IGVertex* v = toBeSearched.top();
			toBeSearched.pop();

			std::vector<IGEdge*> inEdges = v->inEdges;
			for (size_t i = 0; i < inEdges.size(); ++i) {
				IGVertex* src = inEdges[i]->source;

				// Stop at phi node.
//                PHINode* phiNode = isPHINode(src->value);
//                if (phiNode && !isPINode(phiNode))
//                    continue;
				VertexType vt = src->type;
				if (vt == Phi)
					continue;

				std::pair<bool, int> res = isConstInt(src->value);
				if (res.first)
					maxVal = std::min(maxVal, inEdges[i]->weight + res.second);

				if (searched.count(src) == 0)
					toBeSearched.push(src);
				searched.insert(src);
			}
		}

		return maxVal;
#endif
	}

private:
	map<Triple, Result> C;
	map<Value*, int> active;

	Result prove(Value* a, Value* v, int c) {
#if 0
    errs() << "a: ";
    a->print(errs());
    errs()<< '\n';
    errs() << "v: ";
    v->print(errs());
    errs() << '\n';
    errs() << "c: " << c << '\n';
#endif 
		ConstantInt* ac = dyn_cast<ConstantInt>(a);
		ConstantInt* vc = dyn_cast<ConstantInt>(v);
		if (ac && vc)
			if (vc->getSExtValue() - ac->getSExtValue() <= (int64_t) c)
				return True;
			else
				return False;
		for (map<Triple, Result>::iterator i = C.begin(), e = C.end(); i != e;
				++i) {
			const Triple& t = i->first;
			if (t.v == v && t.a == a && t.c <= c && i->second == True)
				return True;
		}

		for (map<Triple, Result>::iterator i = C.begin(), e = C.end(); i != e;
				++i) {
			const Triple& t = i->first;
			if (t.v == v && t.a == a && t.c >= c && i->second == False)
				return False;
		}

		for (map<Triple, Result>::iterator i = C.begin(), e = C.end(); i != e;
				++i) {
			const Triple& t = i->first;
			if (t.v == v && t.a == a && t.c <= c && i->second == Reduced)
				return Reduced;
		}
		if (a == v && c >= 0)
			return True;

		if (getVertex(v) == 0)
			return False;
		if (getVertex(v)->inEdges.size() == 0)
      if (getVertex(v)->type == None)
        return False;

		if (active.count(v) > 0) {
			if (c > active[v])
				return False;
			else
				return Reduced;
		}

		active[v] = c;
		Triple t(a, v, c);
//		PHINode* phi = dyn_cast<PHINode>(v);
//		bool isPHINode = (phi!=0);
//		if(isPHINode)
//			isPHINode = (phi->getNumIncomingValues()>1);

		IGVertex* vertex = getVertex(v);
//    errs() << "type: " << vertex->type << '\n';
		switch (vertex->type) {
		case None:
			C[t] = False;

			for (unsigned int i = 0; i < vertex->inEdges.size(); ++i) {
				C[t] = join(C[t],
						prove(a, vertex->inEdges[i]->source->value,
								c - vertex->inEdges[i]->weight));
			}
			break;
		case Phi: 
			C[t] = True;

			for (unsigned int i = 0; i < vertex->inEdges.size(); ++i) {
				C[t] = meet(C[t],
						prove(a, vertex->inEdges[i]->source->value,
								c - vertex->inEdges[i]->weight));
			}
			break;
		case Add: {
			AddVertex* add = static_cast<AddVertex*>(vertex);
			if (add == 0) {
				errs()
						<< "Something wrong with vertex insertion. The vertex class does not match the type field";
				exit(1);
			}
			int lmax = getMaxValue(add->LHS);
			int rmax = getMaxValue(add->RHS);
#if 0
      errs() << "lmax: " << lmax << '\n';
      add->LHS->print(errs());
      errs() << '\n';
      errs() << "rmax: " << rmax << '\n';
      errs() << '\n';
      add->RHS->print(errs());
#endif
			if (ac == 0) {
				errs()
						<< "Currently we don't support instructions like x+y<c, where c is not a constant!";
				exit(1);
			}
			if (lmax + rmax - ac->getSExtValue() <= (int64_t) c)
				C[t] = True;
			else
				C[t] = False;
			break;
    }
		case Mul: {
			MulVertex* mul = static_cast<MulVertex*>(vertex);
			if (mul == 0) {
				errs()
						<< "Something wrong with vertex insertion. The vertex class does not match the type field";
				exit(1);
			}
			Value* coeffVar = mul->Coeff;
			ConstantInt* coeffCon = dyn_cast<ConstantInt>(coeffVar);
			if (coeffCon == 0) {
				errs() << "Currently we don't support float numbers!";
				exit(1);
			}
			int coeff = coeffCon->getSExtValue();
			C[t] = False;
			for (unsigned int i = 0; i < vertex->inEdges.size(); ++i) {
				C[t] = join(C[t],
						prove(a, vertex->inEdges[i]->source->value,
								c - vertex->inEdges[i]->weight));
			}
			if (coeff == 0) {
				if (0 <= ac->getSExtValue() + c)
					C[t] = join(C[t], True);
			} else {
        Constant* temp_const = ConstantInt::get(ac->getType(), ac->getSExtValue() / coeff);
				C[t] = join(C[t], prove(temp_const, mul->Var, c / coeff));
			}
			break;
    }
		}
		active.erase(v);

		return C[t];
	}

	IGVertex* getVertex(Value* v) {
		return vertices[v];
	}

	Result meet(Result a, Result b) {
		return Result(std::min(a, b));
	}

	Result join(Result a, Result b) {
		return Result(std::max(a, b));
	}
};

}

#endif

